Search for: All records

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with artificial intelligence (AI) components. Specifically, machine learning (ML) components in cyber-physical systems (CPS), such as feedforward neural networks used as feedback controllers in closed-loop systems are considered, which is a class of systems classically known as intelligent control systems, or in more modern and specific terms, neural network control systems (NNCS). We more broadly refer to this category as AI and NNCS (AINNCS). The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2021. In the third edition of this AINNCS category at ARCH-COMP, three tools have been applied to solve seven different benchmark problems, (in alphabetical order): JuliaReach, NNV, and Verisig. JuliaReach is a new participant in this category, Verisig participated previously in 2019 and NNV has participated in all previous competitions. This report is a snapshot of the current landscape of tools and the types of benchmarks for which these tools are suited. Due to the diversity of problems, lack of a shared hardware platform, and the early stage of the competition, we are not ranking tools in terms of performance, yet the presented results combined with 2020 results probably provide the most complete assessment of current tools for safety verification of NNCS. 

This article addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid/tanh activations and use the fact that the sigmoid/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including comparisons with alternative approaches based on mixed integer linear programming as well as on star sets. 

This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network's hybrid system with the plant's, we transform the problem into a hybrid system verification problem which can be solved using state-of-the-art reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if Schanuel's conjecture is true. We evaluate the applicability and scalability of Verisig in two case studies, one from reinforcement learning and one in which the neural network is used to approximate a model predictive controller. 

This paper considers the problem of continuous state estimation from discrete context-based measurements. Context measurements provide binary information as obtained from the system’s environment, e.g., a medical alarm indicating that a vital sign is above a certain threshold. Since they provide state infor- mation, these measurements can be used for estimation purposes, similar to standard continuous measurements, especially when standard sensors are biased or attacked. Context measurements are assumed to have a known probability of occurring given the state; in particular, we focus on the probit function to model threshold-based measurements such as the medical-alarm scenario. We develop a recursive context-aware filter by approx- imating the posterior distribution with a Gaussian distribution with the same first two moments as the true posterior. We show that the filter’s expected uncertainty is bounded when the probability of receiving context measurements is lower-bounded by some positive number for all system states. Furthermore, we provide an observability-like result – all eigenvalues of the filter’s covariance matrix converge to 0 after repeated updates if and only if a persistence of excitation condition holds for the context measurements. Finally, in addition to simulation evaluations, we applied the filter to the problem of estimating a patient’s blood oxygen content during surgery using real-patient data.